Nuprl Lemma : length_cons
11,40
postcript
pdf
A
:Type,
a
:
A
,
as
:(
A
List). ||cons(
a
;
as
)|| = (||
as
|| + 1)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Y
,
||
as
||
Lemmas
length
wf1
origin
A:Type, a:A, as:(A List). ||cons(a; as)|| = (||as|| + 1) A:Type, a:A, as:(A List). ||cons(a; as)|| = (||as|| + 1) 
Tx:A. B(x)